Inference at * 1 0 4 
Iof proof for Lemma eq int cases test:



1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
8.   Type
9. (i = j)  
10. bb:. ((i = j) = bb)  Type
  P(if (i = j) then x else y fi ) 

latex

 by (\p. 
let i = get_int_arg `i` p 
in let x = get_term_arg `x` p 

inin let e = get_term_arg `e` p 
in let A = get_term_arg `A` p 
in 
inAssertAtHyp 
inAi 
inA(
imk_exists_term (dv x) A (mk_equal_term A e x)) 
imkp) 

latex

i1: .....assertion..... NILNIL

i1:   bb:. ((i = j) = bb)
i2: 

i2: 7. bb:. ((i = j) = bb)
i2: 8. P(if (i = j) then x else y fi )
i2: 9.   Type
i2: 10. (i = j)  
i2: 11. bb:. ((i = j) = bb)  Type
i2:   P(if (i = j) then x else y fi )
i.

Definitions

s = t, x:A. B(x), , t  T, (i = j), if b then t else f fi , f(a), , , x:AB(x), Type